'''
Created on 2011-09-06

@author: kacper
'''
import unittest
from dataStructs.formulaSet import Theory
from parsing.parser import sents_parse_string
from dataStructs.definitions import Const, Var


class Test(unittest.TestCase):


    def setUp(self):
        pass


    def tearDown(self):
        pass


    def testSimpleGet(self):
        fo1 = sents_parse_string("A || B || A || B")[0]
        lst = fo1.getVariables()
        self.assertEqual(2,len(lst))
        self.assertTrue(Var('A') in lst)
        self.assertTrue(Var("B") in lst)
        
    def testSimpleGet2(self):
        fo1 = sents_parse_string("((A || B) || (A || B)) && C -> W")[0]
        lst = fo1.getVariables()
        self.assertEqual(4,len(lst))
        print lst
        self.assertTrue(Var('A') in lst)
        self.assertTrue(Var("B") in lst)
       

    def testSimpleGetNot(self):
        fo1 = sents_parse_string("~(~((A || B) || (A || B)) && C -> W)")[0]
        lst = fo1.getVariables()
        self.assertEqual(4,len(lst))
        print lst
        self.assertTrue(Var('A') in lst)
        self.assertTrue(Var("B") in lst)
       
if __name__ == "__main__":
    #import sys;sys.argv = ['', 'Test.testSimpleGet']
    unittest.main()